Model-based testing (MBT) is a well-known approach to automating the testing of hardware and software systems. Instead of writing tests by hand, an abstract model of desired system behavior (henceforth referred to as the model) is used to check that the system under test (henceforth referred to as the system) conforms to this behavior; the model can be used either offline (using it to generate in advance a sequence of stimuli and anticipated responses) or online (using it explicitly during the testing process).
In MBT, a test is typically specified by describing the set of states to be explored by the test. In a deterministic system, where the model specifies the precise state resulting from any stimulus, it is straightforward to construct a sequence of inputs that will explore (i.e. drive the system to) every state in this set (assuming such an exploration is possible), and known optimization techniques can be used to design such an exploration so as to minimize the cost of the resulting test execution.
Most real specifications, however, require nondeterministic models in which the system is allowed to move to a plurality of states in response to a stimulus. Such nondeterminism can arise for several reasons. One reason is to allow the model to describe a variety of potentially suitable system implementations. Another reason is to allow the system to behave in alternative ways when facing exhaustion of resources such as memory. Another reason is to allow more efficient concurrent implementations in which data races introduce nondeterministic system behavior.
In testing that a system meets a nondeterministic specification, it is often assumed that the system is fair to each transition of the specification (i.e., the system will make every possible nondeterministic choice if given enough opportunities). But in fact, some transitions might be unlikely or impossible for a given implementation. Under these circumstances, common MBT techniques (e.g., generating a pre-computed tour of the state space) often lead to wasted test cycles and poor test coverage.